A:Type, x,y:A, P:(A), i,j:.
(P(if (i = j) then x else y fi ))  (P(if (i = j) then x else y fi )) 

latex

ProofTree

Definitions	t  T, P  Q, , x:A. B(x), x:A. B(x), ff, tt, if b then t else f fi , Unit, , False, A, a  b  T ,
Lemmas	eq int wf, ifthenelse wf, eq int eq false elim, eq int eq true elim, bool wf